Lambda the Ultimate

No we haven’t lost our mind! We know that compilers and the languages they represent are the absolute foundation of computing. Compilers are so basic and originate so early in the history of computers it is easy to forget what a compiled language really is: A compiled language is simply an extension of the machine codes defining the register machine. As long as we insist that a language compile we are insisting that the register machine must be our computing architecture. This is because no matter how we disguise it the basic properties of the register machine will leak through into any language that must compile directly without an intervening virtual machine.

The property we are most concerned about is “flow”. We read and execute one instruction after another in order. If we need to execute a different string of instructions we use conditional jump instructions. On a higher level a conditional jump would be a goto statement with a label. Goto’s are very powerful but may lead to what we used to call “spaghetti code”. It can be impossible to “see” where the program is going next. We bring this up because “spaghetti code” still lives in the form of if/then/else statements, but is more subtle.

Another example of the “flow” problem is that the code must be analytic. The register machine has no built in way to back up or recover from errors. We can and must check for errors but the only option then is usually to terminate the program. The logic has been broken! The analytic assumption is reasonable as long as the program is not connected to the external world somehow, perhaps through user inputs, sockets, or external activity. The need to be analytic leads the “fortress” mentality; radical steps to ensure that the code is analytic.

A solution exists that we like to call synthetic logic. A synthetic logic is a set of event rules with a works or doesn’t work logic. Synthetic logic is a logic of possibility; the event X is said to work if events A, B, and C work in order. If something goes wrong the system simply backs up to the starting point automatically without any specific error processing. Synthetic logic can work along with an analytic true or false logic. The dilemma is that synthetic logic in whatever form will require a virtual machine to execute because it will be based on backward or forward chaining control. In other words it won’t compile on a register machine.

It seems to us that language designers must address the larger problem of languages that are hard to compile or impossible to compile. These languages usually don’t make it into prime time because they don’t compile. If we continue to insist that mainstream languages compile we will simply be getting more of the same subtle problems. In the search for the ultimate language the compiler should not be a consideration. Any language concept can be implemented as a virtual machine. With the fast computers that we have today this may be all that is needed. If that language should actually turn out to be the ultimate language then there would be plenty of money to design a machine on which it could be compiled directly.

Some of you might be interested in the following Conference during the first weekend in June at UBC in Vancouver, Canada:

Conference: Foundational Methods in Computer Science (FMCS05)

Local organizer: John MacDonald
Location: All sessions are held in WMAX 110 - 1933 West Mall
Dates: June 3-5, 2005

Friday, June 3, 2005

9:00-10:30a.m. Ernie Manes, UMass Amherst, USA
From locally-Boolean rings to sum-ordered categories

11:00-12:30p.m. Vaughan Pratt, Stanford University, USA
Recent developments in Chu spaces

2:30-4:00p.m. Steve Bloom, Stevens Institute of Technology, USA
Regular words

4:30-6:00p.m. Robin Cockett, University of Calgary
Restriction Categories and Ehresmann's Theorem

Saturday, June 4, 2005

9:00-9:50a.m. Paul Taylor, Manchester, UK
Extension of ASD (from locally compact locales) to and
beyond general locales

9:50-10:30a.m. Cyrus Nourani, USA
Functorial Model Computations

11:00-11:30a.m TBA

11:30-12:15p.m. Art Stone, Vancouver, Canada
2-Dimensional Adjunctions

2:00-2:30p.m. Varmo Vene, University of Tartu, Estonia
Signals and Comonads

2:30-3:00p.m. Bob Rosebrugh, Mt. Allison University
TBA

3:00-3:30p.m. Chris Dutchyn, University of British Columbia
Aspects are Dual to Objects

4:00-5:00p.m. Philip Mulry, Colgate University, USA
Monad Compositions on Recursive Data Types

Sunday, June 5, 2005

9:00- 9:30a.m. Brian Redmond, University of Ottawa,
Categorical Models for Soft Linear Logic

9:30-10:00a.m. X. Guo, University of Calgary,
Range Restriction Categories

10:00-10:30a.m. Dana Harrington, University of Calgary
TBA

10:30-11:00a.m. Break

11:00-11:30a.m. David Oury, McGill University,
TBA

11:30-12:00 Pieter Hofstra, University of Ottawa,
TBA

12:00-12:30p.m. TBA

Last updated: 5/27/05

For further information see the conference website:
http://www.pims.math.ca/science/2005/05fmcs

I just came accross this interesting paper: Pure bigraphs: structure and dynamics. From the abstract:

"...it is shown that behavioural
analysis for Petri nets, pi-calculus and mobile ambients can all
be recovered in the uniform framework of bigraphs."

An interesting thing from my point of view is that an attempt is made to provide a descriptive explanation of the material, obviously along with math proofs.


There are also three, very basic, audio lectures(!) on pi-calculus at the following site: http://courses.cs.vt.edu/~cs5204/fall03/DayByDay.html.

Hi, I'm looking for some short algorithms that use state in tricky ways, where by "tricky" I mean:

1. State is used nonlinearly. That is, there should be multiple pointers to some of the state in the program.

2. The state should be "visible" to clients. Something like memoizing or caching is stateful and nonlinear, but it has no visible side-effects.

3. The state should have an indefinite lifetime -- that is, stack allocation isn't a sufficient memory management strategy.

4. Ideally, the state should be higher-order -- I'd like to see references of function (or object) types, so that there's a pointer to code. This is less critical than the others, but still nice.

Any ideas? I've thought of union-find, and I would guess there are graph algorithms that have these properties, but I'm relatively ignorant about them.

Hi everyone,

I need to perform a data flow analysis on a lamda-calculus like functional language.

Ideally, this should be a type-based approach. Can anyone on this forum direct me a mean to do this.

What is particularly troublesome is that a data flow analysis naturally necessitates a fix-point analysis which is done recursively on the structure of the program whereas a type analysis is done in one pass over the program.

I would be grateful for any insight anyone might have to help me solve this problem.

R.K.